E:Type, dE:EqDecider(E), dL:EqDecider(IdLnk), V:(KndIdType), pred?:(E(E+Unit)),
info:(E(IdId+(IdLnkE)Id)), val:(e:EV(kind(e),loc(e))),
p:(e:E, l:IdLnk.
p:(e':E.
p:(e'':E.
p:(rcv?(e'')
p:( sender(e'') = e
p:( link(e'') = l
p:( e'' = e'  e'' < e' & loc(e') = destination(l)  Id), e:E, l:IdLnk.
SWellFounded(first(y) & x = pred(y)  E)
 sends(dE;dL;pred?;info;val;p;e;l)  Msg_sub(l;l,tg. V(rcv(l,tg),destination(l))) List 

latex

Definitions

SWellFounded(R(x;y)), x,y. t(x;y), A, first(e), pred(e), x:A. B(x), rcv?(e), sender(e), link(e), P  Q, e < e', Prop, kind(e), loc(e), Unit, Knd, EqDecider(T), Msg_sub(l;M), sends(dE;dL;pred?;info;val;p;e;l), map(f;as), rcv-from-on(dE;dL;info;e;l;r), IdLnk, rcv(l,tg), destination(l), receives(dE;dL;pred?;info;p;e;l), b, Msg(M), P  Q, Id, A & B, P & Q, P  Q, rmsg(info;val;e), haslink(l;m), x:A. B(x), t  T

Lemmas

haslink wf, rmsg wf, assert-rcv-from-on, Id wf, receives wf, ldst wf, rcv wf, Msg wf, rcv-from-on wf, assert wf, map wf, deq wf, IdLnk wf, Knd wf, unit wf, loc wf, kind wf, cless wf, link wf, sender wf, rcv? wf, pred wf, first wf, not wf, strongwellfounded wf